1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

use biodivine_lib_param_bn::biodivine_std::traits::Set;
use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};

use crate::algorithms::eval_dynamic::_attractors::itgr::{
    BwdProcess, FwdProcess, Process, Scheduler,
};
use crate::algorithms::eval_dynamic::_attractors::saturated_reachability::reachability_step;

impl BwdProcess {
    pub fn new(initial: GraphColoredVertices, universe: GraphColoredVertices) -> BwdProcess {
        BwdProcess {
            universe,
            bwd: initial,
        }
    }

    pub fn get_reachable_set(&self) -> &GraphColoredVertices {
        &self.bwd
    }
}

impl FwdProcess {
    pub fn new(initial: GraphColoredVertices, universe: GraphColoredVertices) -> FwdProcess {
        FwdProcess {
            universe,
            fwd: initial,
        }
    }

    pub fn get_reachable_set(&self) -> &GraphColoredVertices {
        &self.fwd
    }
}

impl Process for BwdProcess {
    fn step(&mut self, scheduler: &mut Scheduler, graph: &SymbolicAsyncGraph) -> bool {
        reachability_step(
            &mut self.bwd,
            &self.universe,
            scheduler.get_active_variables(),
            |var, set| graph.var_pre(var, set),
        )
    }

    fn weight(&self) -> usize {
        self.bwd.symbolic_size()
    }

    fn discard_states(&mut self, set: &GraphColoredVertices) {
        self.universe = self.universe.minus(set);
        self.bwd = self.bwd.minus(set);
    }
}

impl Process for FwdProcess {
    fn step(&mut self, scheduler: &mut Scheduler, graph: &SymbolicAsyncGraph) -> bool {
        reachability_step(
            &mut self.fwd,
            &self.universe,
            scheduler.get_active_variables(),
            |var, set| graph.var_post(var, set),
        )
    }

    fn weight(&self) -> usize {
        self.fwd.symbolic_size()
    }

    fn discard_states(&mut self, set: &GraphColoredVertices) {
        self.universe = self.universe.minus(set);
        self.fwd = self.fwd.minus(set);
    }
}